open util/ordering[State]

abstract sig Ser {
	come : set Ser
}
one sig Barqueiro, Couve, Ovelha, Lobo extends Ser {}

fact {
	come = Lobo -> Ovelha + Ovelha -> Couve
	last.dir = Ser
}

pred show[]{}

run show for 10 but exactly 10 State

assert cenas{
	no s:State | s.dir = Ser && s!=last
}

check cenas for 10 but exactly 10 State


sig State {
	esq : set Ser,
	dir : set Ser
}

pred margem[s : set Ser] {
	some (s.come & s) => Barqueiro in s
}

pred inv[s : State] {
	s.esq + s.dir = Ser
	no (s.esq & s.dir)
	margem[s.esq] and margem[s.dir]
}

fact {
	all s : State | inv[s]
	first.esq = Ser
	all s : State, s' : s.next | some c : Ser | atravessa[s,s',c]
}

pred atravessa[s,s' : State, c : Ser] {
    let cs = Barqueiro + c {
	  cs in s.esq => s'.esq = s.esq - cs and s'.dir = s.dir + cs
                     else s'.dir = s.dir - cs and s'.esq = s.esq + cs
	}
}

run { last.dir = Ser} for 3 but exactly 7 State
